{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

-----------------------------------------------------------------------------
-- |
-- Maintainer  :  joost.visser@di.uminho.pt, alcino@di.uminho.pt
-- Stability   :  experimental
-- Portability :  portable
--
-- See
--
--     Type-safe Two-level Data Transformation
-- 
-- by
--
--     Alcino Cunha, Jose Nuno Oliveira, Joost Visser
--
-----------------------------------------------------------------------------

module Data.Transform.TwoLevel where

import Data.Set as Set
import Data.Map as Map
import Data.List as List
import Control.Monad.State
import Data.Maybe
import Data.Transform.Type hiding ((/\))
         
-----------------------------------------------------------------------------
-- * Encapsulation of type-changing transformations

-- | Pairs of bi-directional value-level data transformation functions.
data Rep a b = Rep {to :: a -> b, from :: b -> a}

-- | The View constructor expreses that a type a can be represented by
--   a type b, as witnessed by value-level functions that convert 
--   between these types. Note that the target type does not escape, 
--   which means that it is implicitly existentially qualified.
data View a where
    View :: Rep a b -> Type b -> View (Type a)

instance Show (View a) where
    show (View _ b) = "(View (Rep <to> <from>) "++(show b)++")"

-- | Print the string representation of the target type encapsulated in a view.
showType :: View a -> String
showType (View _ b) = show b

-- | Type-changing rewrite rules.
type Rule = forall a . Type a -> Maybe (View (Type a))

-----------------------------------------------------------------------------
-- * Strategy combinators for two-level transformations

-- | Sequential composition.
(>>>) :: Rule -> Rule -> Rule
(f >>> g) a = do View r b <- f a
                 View s c <- g b
                 return (View (comprep r s) c)

-- | Left-biased choice.
(|||) :: Rule -> Rule -> Rule
(f ||| g) x = f x `mplus` g x

-- | Do-nothing operation. 
--   Unit for sequential composition. 
--   Left-zero and right-unit for left-biased choice.
nop :: Rule
nop x = Just (View idrep x)

-- | Repeat until failure.
--   Zero or more repetitions.
many :: Rule -> Rule
many r = (r >>> many r) ||| nop

-- | Apply argument rule exactly once, at arbitrary depth.
once :: Rule -> Rule
once r Int  = r Int
once r Bool = r Bool
once r Char = r Char
once r One  = r One
once r String = r String
once r (List a) = r (List a) `mplus` 
                  (do View s b <- once r a
                      return (View (maprep s) (List b)))
once r (Set a) = r (Set a) `mplus` 
                 (do View s b <- once r a
                     return (View (maprep s) (Set b)))
once r (Map a b) = r (Map a b) `mplus`
                   (do View s c <- once r a
                       return (View (bimaprep s idrep) (Map c b))) `mplus`
                   (do View s c <- once r b
                       return (View (bimaprep idrep s) (Map a c)))
once r (Either a b) = r (Either a b) `mplus`
                      (do View s c <- once r a
                          return (View (bimaprep s idrep) (Either c b))) `mplus`
                      (do View s c <- once r b
                          return (View (bimaprep idrep s) (Either a c)))
once r (Prod a b) = r (Prod a b) `mplus`
                    (do View s c <- once r a
                        return (View (bimaprep s idrep) (Prod c b))) `mplus`
                    (do View s c <- once r b
                        return (View (bimaprep idrep s) (Prod a c)))
once r (Tag n a) = r (Tag n a) `mplus` 
                   (do View s b <- once r a
                       return (View s (Tag n b)))
once r (TInv t i)
   = r (TInv t i) `mplus` 
     (do View s b <- once r t
         let inv' = COMP t i (FUN "from" (from s))
         return $ View s (TInv b inv')
     )
once r x = r x

----------------------------------------
-- ** Value-level combinators used to define two-level combinators.

-- | Pair of identity value-level tranformations. Used to define 'nop'.
idrep :: Rep a a
idrep = Rep {to = id, from = id}

-- | Sequential composition of value-level transformations.
--   Used to define '(>>>)'.
comprep :: Rep a b -> Rep b c -> Rep a c
comprep f g = Rep {from = (from f) . (from g), to = (to g) . (to f)}

-- | Lift value-level transformations to a functor.
--   Used to define traversal strategies, like 'once'.
maprep :: Functor f => Rep a b -> Rep (f a) (f b)
maprep r = Rep {to = fmap (to r), from = fmap (from r)}

-- Additional instances of Functor. Needed because of maprep.
instance Functor Set where
    fmap = mapMonotonic

-- | Lift value-level transformations to a bi-functor.
--   Used to define traversal strategies, like 'once'.
bimaprep :: Bifunctor f => Rep a b -> Rep c d -> Rep (f a c) (f b d)
bimaprep x y = Rep {to = bimap (to x) (to y), from = bimap (from x) (from y)}

-- | Class of bi-functors. Needed for 'bimaprep'
class Bifunctor f where
    bimap :: (a -> b) -> (c -> d) -> f a c -> f b d

instance Bifunctor (,) where
    bimap = (><)

instance Bifunctor Either where
    bimap = (-|-)

instance Bifunctor Map where
    bimap f g = mapKeysMonotonic f . Map.map g

-----------------------------------------------------------------------------
-- * Unleashing composed data migration functions

-- | Apply the forward value-level function masked by a view.
forth :: View (Type a) -> Type b -> a -> Maybe b
forth (View rep tb') tb a = do {Eq <- teq tb tb'; return (to rep a)}

-- | Apply the backward value-level function masked by a view.
back :: View (Type a) -> Type b -> b -> Maybe a
back (View rep tb') tb b = do {Eq <- teq tb tb'; return (from rep b)}

-- | Take the forward and backward value-level functions out of
--   a view.
unView :: View (Type a) -> Type b -> (a -> Maybe b, b -> Maybe a)
unView (View rep tb') tb =
  ( \a -> do {Eq <- teq tb tb'; return (to rep a)}
  , \b -> do {Eq <- teq tb tb'; return (from rep b)} )

-----------------------------------------------------------------------------
-- * Rules for format evolution

----------------------------------------
-- ** Enrichment and removal

-- | Type of generic value-level queries.
type Query b = forall a . Type a -> a -> b

-- | Add a field.
--   The forward value-level function inserts a field
--   determined by a query on its input value.
addinfo :: Type b -> Query b -> Rule
addinfo b f a = Just (View rep (Prod a b))
    where rep = Rep {to = \y -> (y,f a y), from = fst}

----------------------------------------
-- ** Generalization and restriction

-- | Add alternative.
--   The backward value level function fails if the added 
--   alternative is present.
addalt :: Type b -> Rule
addalt b a = return $ View rep (Either a b)
    where rep = Rep {to = Left, from = \(Left x) -> x}

-- | Allow repetition.
--   Maps optional to a list.
allowRep :: Rule
allowRep (Either a One) = return $ View (Rep opt2seq seq2opt) (List a)
  where 
    opt2seq (Left x) = [x]
    opt2seq (Right ()) = []
    seq2opt []  = Right ()
    seq2opt [x] = Left x
    seq2opt _ = error "Too many elements in list for conversion to optional"
allowRep _ = mzero

-- | Lifted version of 'allowRep', works on functors.
allowRep1 :: Rule
allowRep1 a = return $ View rep (Mu ((K a) :+: ((K a) :*: Id)))
  where 
    rep = Rep singleton (nehead . out)
    singleton x = In $ Inl $ Const x
    nehead (Inl x) = unConst x
    nehead (Inr y) = error "Too many elements in list+"

----------------------------------------
-- ** Focus on tags

-- | Perform the argument rule inside the given tag.
inside :: String -> Rule -> Rule
inside n r (Tag m a) | n==m = do View r b <- r a
                                 return $ View r (Tag m b)
inside _ _ _ = Nothing

-- | Perform the argument rule on the given tag.
atTag :: String -> Rule -> Rule
atTag n r x@(Tag m a) | n==m = r x
atTag _ _ _ = Nothing

-----------------------------------------------------------------------------
-- * Rules for data mapping

-- | Flatten a hierarchical data type.
--   Does not include the rule for recursion elimination.
flatten :: Rule
flatten = many (aux >>> many aux >>> prods)
    where aux = once (listmap ||| mapsum ||| summap ||| mapprodmap ||| setmap ||| prodsum ||| sumone ||| prodone)

-- | Map a hierarchical datatype to a relational type.
toRDB :: Rule
toRDB = many (once fixastable) >>> many (once enum2int) >>> removetags >>> flatten

----------------------------------------
-- ** Elimination and introduction

-- | Eliminate list by refinement to map.
listmap :: Rule
listmap (List a) = Just (View rep (Map Int a))
  where
    rep = Rep {to = seq2index, from = list}
    list :: Map Int a -> [a]
    list = Map.elems
    seq2index :: [a] -> Map Int a
    seq2index = Map.fromList . (zip [0..])
listmap _ = Nothing

-- | Eliminate set by refinement to map.
setmap :: Rule
setmap (Set a) = return $ View rep (Map a One) 
  where 
    rep :: Rep (Set a) (Map a ())
    rep = Rep {to = set2fm, from = dom}
    set2fm s = Map.fromDistinctAscList (zip (Set.toAscList s) (repeat ()))
    dom = Set.fromDistinctAscList . keys
setmap _ = Nothing

-- | Eliminate optional by refinement to map.
sumone :: Rule
sumone (Either a One) = return $ View plusone (Map One a)
 where
  plusone :: Rep (Either a ()) (Map () a)
  plusone = Rep {to = optintro, from = optelim}
    where optintro (Left x) = Map.singleton () x
	  optintro (Right ()) = Map.empty
	  optelim m | Map.member () m = let Just x = Map.lookup () m in Left x
		    | otherwise = Right ()
sumone _ = fail "Not applicable"




----------------------------------------
-- ** Distribution

-- | Distribute map over sum.
mapsum :: Rule
mapsum (Map a (Either b c)) = return $ View rep (Prod (Map a b) (Map a c))
  where
    rep = Rep {to = uncojoin, from = cojoin a}
    uncojoin :: Map a (Either b c) -> (Map a b, Map a c)
    uncojoin = (  fmap (either id undefined) . Map.fromDistinctAscList >< 
                  fmap (either undefined id) . Map.fromDistinctAscList) .
               List.partition (isLeft . snd) . Map.toAscList
    -- Pre: non duplicate keys
    cojoin :: Type a -> (Map a b, Map a c) -> Map a (Either b c)
    cojoin t = Map.fromDistinctAscList . 
               sortBy (\x y -> gcompare t (fst x) (fst y)) .
               uncurry (++) . 
               (Map.toAscList . fmap Left >< Map.toAscList . fmap Right)
mapsum _ = Nothing

-- | Distribute product over sum.
prodsum :: Rule
prodsum (Prod a (Either b c)) = return $ View distr (Either (Prod a b) (Prod a c))
 where
  distr :: Rep (a,Either b c) (Either (a,b) (a,c))
  distr = Rep {from = undistr, to = distr}
    where distr (x, Left y) = Left (x,y)
          distr (x, Right y) = Right (x,y)
          undistr (Left (x,y)) = (x, Left y)
          undistr (Right (x,y)) = (x, Right y)
prodsum (Prod (Either b c) a) = return $ View distl (Either (Prod b a) (Prod c a))
 where
  distl :: Rep (Either b c, a) (Either (b,a) (c,a))
  distl = Rep {from = undistl, to = distl}
    where distl (Left y,x) = Left (y,x)
          distl (Right y,x) = Right (y,x)
          undistl (Left (y,x)) = (Left y,x)
          undistl (Right (y,x)) = (Right y,x)
prodsum _ = Nothing

summap :: Rule
summap (Map (Either a b) c) = return $ View eithermap (Prod (Map a c) (Map b c))
  where
    eithermap :: Rep (Map (Either a b) c) (Map a c, Map b c)
    eithermap = Rep {to = unpeither, from = peither}
    unpeither = ( mapKeysMonotonic (either id undefined) . Map.fromDistinctAscList >< 
                  mapKeysMonotonic (either undefined id) . Map.fromDistinctAscList
                ) . List.partition (isLeft . fst) . Map.toAscList
    peither = Map.fromDistinctAscList . uncurry (++) . 
              (fmap (Left >< id) . Map.toAscList >< fmap (Right >< id) . Map.toAscList)
summap _ = Nothing





----------------------------------------
-- ** Split, join

-- | Split and join.
mapprodmap :: Rule
mapprodmap (Map a (Prod b (Map c d))) 
  = return $ View (mapcomposite a) (Prod (Map a b) (Map (Prod a c) d))
 where
  -- Precondition to from: all keys a in second table must exist in the first
  mapcomposite :: Type a -> Rep (Map a (b, Map c d)) (Map a b, Map (a,c) d)
  mapcomposite t = Rep {to = unnjoin, from = njoin}
    where unnjoin = (Map.map fst /\ to (mapcomp t) . Map.map snd)
          njoin = Map.fromDistinctAscList . uncurry myzip . (Map.toAscList >< Map.toAscList . from (mapcomp t))
          myzip l [] = fmap (id >< (id /\ const Map.empty)) l
          myzip ((x,y):l) ((z,w):m) | gcompare t x z == EQ = (x,(y,w)) : myzip l m
                                    | otherwise = (x,(y,Map.empty)) : myzip l ((z,w):m)
  unnjoin :: Map a (Map b c) -> Map (a,b) c
  unnjoin =  Map.fromDistinctAscList . concat . 
             List.map ((\ (x,l) -> List.map ((const x /\ id) >< id) l) . 
             (id >< Map.toAscList)) . 
             Map.toAscList
  njoin :: Type a -> Map (a,b) c -> Map a (Map b c) 
  njoin t = Map.fromDistinctAscList . 
            fmap (fst.fst.head /\ Map.fromDistinctAscList . fmap (snd >< id)) . 
            groupBy aux . Map.toAscList
    where aux x y = gcompare t (fst (fst x)) (fst (fst y)) == EQ
  mapcomp :: Type a -> Rep (Map a (Map c d)) (Map (a,c) d)
  mapcomp t = Rep {to = unnjoin, from = njoin t}
mapprodmap _ = Nothing

----------------------------------------
-- ** Recursion

-- | Type of tables.
type Table f = (Map Int (f Int), Int)

-- | Refine fix-point datatype to table type.
fixastable :: Rule
fixastable (Mu f) = do
  (View (Rep t f) fInt) <- applyF f Int
  let rep = Rep {to = (Map.map t >< id) . fixtotable, from = tabletofix . (Map.map f >< id)}
  return (View rep (Prod (Map Int (fInt)) Int)) 
   where
    fixtotable :: Dist f => Mu f -> Table f
    fixtotable mu = execState (mcata aux mu) (Map.empty,-1)
      where 
        aux :: f Int -> State (Table f) Int
        aux i = do
          (t,k) <- get
          put (Map.insert (k+1) i t, k+1)
          return (k+1)
    -- Precondition to abs: non circular and all keys exist
    tabletofix :: Functor f => Table f -> Mu f
    tabletofix = ana aux
      where 
        aux :: Functor f => Table f -> f (Table f)
        aux (t,k) = fmap (\k -> (t,k)) (fromJust $ Map.lookup k t)
fixastable _ = Nothing

-- | Unlift a functor while applying it to a type.
--   Previously: removefunctors.
applyF :: Fctr f -> Type a -> Maybe (View (Type (f a)))
applyF Id x        = return (View (Rep {to = unIdent, from = Ident}) x)
applyF (K a) x     = return (View (Rep {to = unConst, from = Const}) a)
applyF (g:*:h) x   = do
  (View (Rep g2gx gx2g) gx) <- applyF g x
  (View (Rep h2hx hx2h) hx) <- applyF h x
  let rep = Rep {to = \(Pair x y) -> (g2gx x,h2hx y), from = \(x,y) -> Pair (gx2g x) (hx2h y)}
  return (View rep (Prod gx hx))
applyF (g:+:h) x = do
  (View (Rep g2gx gx2g) gx) <- applyF g x
  (View (Rep h2hx hx2h) hx) <- applyF h x
  let rep = Rep {to = (g2gx-|-h2hx) . aux, from = xua . (gx2g-|-hx2h)}
  return (View rep (Either gx hx))
      where 
        aux (Inl x) = Left x
        aux (Inr x) = Right x
        xua (Left x)  = Inl x
        xua (Right x) = Inr x
applyF (g:@:h) x   = do 
  (View (Rep to from) hx) <- applyF h x
  let rep = Rep (fmap to . unComp) (Comp . fmap from)
  return (View rep (g hx))

-- | Derive the functor for a given type.  
class Functor f => FunctorOf t f | t -> f where
  functorOf :: Type t -> Fctr f
instance FunctorOf Int (K Int) where
  functorOf _ = K Int
instance FunctorOf () (K ()) where
  functorOf _ = K One
instance (FunctorOf a f, FunctorOf b g)
 => FunctorOf (a,b) (f:*:g) where
  functorOf (Prod a b) = (functorOf a :*: functorOf b)
instance (FunctorOf a f, FunctorOf b g)
 => FunctorOf (Either a b) (f:+:g) where
  functorOf (Either a b) = (functorOf a :+: functorOf b)
instance FunctorOf a f
 => FunctorOf [a] ([]:@:f) where
  functorOf (List a) = List :@: functorOf a


-----------------------------------------------------------------------------
-- * Associativity and commutativity

-- | Associate product to the right. One step.
assocr :: Rule
assocr (Prod (Prod a b) c) = return $ View aux (Prod a (Prod b c))
    where aux = Rep {to = fst.fst /\ snd><id, from = id><fst /\ snd.snd}
assocr _ = fail "Cannot apply!"

-- | Associate product to the left. One step.
assocl :: Rule
assocl (Prod a (Prod b c)) = return $ View aux (Prod (Prod a b) c)
    where aux = Rep {from = fst.fst /\ snd><id, to = id><fst /\ snd.snd}
assocl _ = fail "Cannot apply!"

-- | Put maps to the right and non-maps to the left.
--   Needs to be redesigned....
prods :: Rule
prods = many (many (once assocr) >>> once swap) >>> many (once assocl)
 where
   swap :: Rule
   swap (Prod a (Map b c)) = fail "Cannot apply!"
   swap (Prod a (Prod (Map b c) d)) = fail "Cannot apply!"
   swap (Prod (Map a b) c) = return $ View (Rep {from = snd/\fst, to = snd/\fst}) (Prod c (Map a b))
   swap _ = fail "Cannot apply!"

-- | Right unit for product.
prodone :: Rule
prodone (Prod a One) = return $ View rep a
 where
  rep :: Rep (a,()) a
  rep = Rep {to = fst, from = \x -> (x,())}
prodone _ = fail "Not applicable"


-----------------------------------------------------------------------------
-- * Miscelaneous rules

-- | Refine an n-sum of taged ones to an integer.
--   In other words, interpret the n-sum as an enumeration type.
enum2int :: Rule
enum2int = (many (once eitherRightAssoc)) >>> e2i 0 where
  e2i :: Int -> Rule
  e2i i (Tag tg One) = do
    -- return (View (Rep (\() -> i) (\i' -> if i==i' then () else error ("Invalid enum: "++(show i)))) Int)
    return (View (Rep (\() -> i) (ifeq () (error "Enum invalid") i)) Int)
  e2i i (Either (Tag tg One) b) = do
    (View rep b) <- e2i (i+1) b
    Eq <- teq Int b
    -- return (View (Rep (either (\() -> i) (\b -> ((to rep) b)+1)) (\i' -> if i==i' then Left () else Right ((from rep) i'))) b)
    return (View (Rep (either (\() -> i) ((to rep))) (ifeq (Left ()) (Right . (from rep)) i)) b)
  e2i _ _ = Nothing
ifeq l r i i' = if i==i' then l else r i'

-- | Associate sums to the right.
--   Used by 'enum2int' to discover enumeration types.
eitherRightAssoc :: Rule
eitherRightAssoc (Either (Either a b) c) = return (View (Rep to from) (Either a (Either b c)))
  where
      to (Left (Left a)) = Left a
      to (Left (Right b)) = Right (Left b)
      to (Right c) = Right (Right c)
      from (Left a) = Left (Left a)
      from (Right (Left b)) = Left (Right b)
      from (Right (Right c)) = Right c
eitherRightAssoc _ = Nothing

-- | Remove all tags from a type represention. This is useful to
--   allow later rules to assume no tags are present.
removetags :: Rule
removetags = many (once aux)
    where aux (Tag n x) = Just (View idrep x)
	  aux _ = Nothing

-----------------------------------------------------------------------------
-- * Auxiliary types and functions

-- | Determine whether the left alternative is present.
isLeft :: Either a b -> Bool
isLeft = either (const True) (const False)

-- | Type of non-empty lists
data List1 a    -- Mu ((K a) :+: ((K a) :*: ID))
  = Singleton a 
  | Cons1 { head1 :: a, tail1 :: (List1 a) }

----------------------------------------
-- ** Pointfree operators

infix 5 ><
infix 4 /\
infix 3 -|-
infix 2 \/

(f >< g) (x,y) = (f x, g y)
(/\) f g x = (f x, g x)
(f -|- g) (Left x) = Left (f x)
(f -|- g) (Right x) = Right (g x)
(\/) f g (Left x) = f x
(\/) f g (Right x) = g x
  
-----------------------------------------------------------------------------
-- * Unleashing conversion functions
    
-- | Variation on 'forth' that does not need static knowledge of the
--   target type, and produces a dynamically typed value instead.
forthDyn :: View (Type a) -> a -> Maybe Dynamic
forthDyn (View rep b) x = return (Dyn b (to rep x))

-- | Variation on 'back' that does not need static knowledge of the
--   original type, and produces a dynamically typed value instead.
backDyn :: View (Type a) -> Dynamic -> Maybe a
backDyn (View rep b) (Dyn c x) = do
  Eq <- teq b c
  return (from rep x)

-----------------------------------------------------------------------------




